Teilprojekt D: Beweistheoretische Semantik

Projektleiter:
Prof. Dr. Peter Schroeder-Heister
Universität Tübingen
Wilhelm-Schickard-Institut für Informatik
Sand 13
72076 Tübingen
Tel.: 07071/29-74284
Fax: 07071/67540
email: schroeder-heister@uni-tuebi ngen.de

Mitarbeiter:
Dr. Reinhard Kahle - email: kahle@informatik.uni-tuebingen.de(kahle@informatik.uni-tuebingen.de)
N.N.

Zusammenfassung

Alternativ zur klassischen Semantik der logischen Folgerung, die auf dem Begriff der Wahrheit in einer mengentheoretischen Struktur aufbaut, soll eine erkenntnistheoretische Konzeption entwickelt werden, die auf den Begriff des Beweises oder der Widerlegung in bezug auf atomare Deduktionsstrukturen zurückgreift. Diese Konzeption beruht (A) auf Inversionsprinzipien, die es erlauben, aus gegebenen Konstruktionsprinzipien für Beweise oder Widerlegungen neue Information zu gewinnen, (B) auf der Idee von logikunabhängigen strukturellen Annahmen, welche die Form des erhaltenen Folgerungsbegriffs wesentlich mitbestimmen. In Teilprojekt A wird im Anschluß an eine systematische Erfassung der bislang vorgeschlagenen Inversionsprinzipien eine Definition von Folgerungsrelationen basierend auf einem Prinzip der "definitorischen Reflexion" unternommen, in Teilprojekt B wird die Abhängigkeit der erhaltenen Systeme von strukturellen Grundannahmen untersucht. Die Durchführbarkeit des geplanten Programms wird als Testfall dafür angesehen, wie weit erkenntnistheoretisch orientierte Ansätze im Bereich der Semantik tragfähig sind. Hat das Projekt den erhofften Erfolg, sollen die entwickelten Ideen in der zweiten Projektphase (ab Januar 2000) zur Modellierung intensionaler Logiken verwendet werden, die einen bevorzugten Anwendungsfall philosophischer Semantiken darstellen.

Ziele

Der Begriff der logischen Folgerung ist der zentrale logische Begriff der Semantik. Daher wird er in das Zentrum des Projekts gestellt. Im Hinblick auf die Signifikanz des Folgerungsbegriffs innerhalb der logischen Semantik unterscheiden sich klassische und beweistheoretische Konzeption nicht.

Die definientia des Folgerungsbegriffs sind jedoch nach klassischer und beweistheoretischer Konzeption grundsätzlich verschieden. Diese Unterschiede liegen im wesentlichen in drei Punkten:

1. An die Stelle des Wahrheitsbegriffs bzw. des Begriffs der Erfüllung tritt der Begriff eines Beweises bzw. eines schematischen Beweises. Dabei ist der Begriff des Beweises nicht als Herleitung in einem formalen System zu verstehen.

2. Die zugrundegelegten atomaren Strukturen sind verschieden. Nach klassischer Konzeption handelt es sich um Bereiche mit mengentheoretisch verstandenen Prädikaten und Relationen. Nach beweistheoretischer Auffassung wählt man Bereiche, deren Struktur durch (material-)deduktive Beziehungen auf atomarer Ebene gegeben ist, z.B. durch eine Abschlußoperation.

3. Die Übertragung des Gültigkeitsbegriffs von atomarer auf komplexe Ebene verwendet verschiedene Prinzipien. Nach klassischer Konzeption benutzt man in der Regel eine mengentheoretische Metasprache, den Begriff der Wahrheit oder Gültigkeit unter einer Belegung der freien Variablen über einem Individuenbereich sowie die Idee der Wahrheitskonservierung bei der Folgerung. In der beweistheoretischen Semantik definiert man die Gültigkeit von Argumentstrukturen durch die Inversion von kanonischen Beweisen; diese Definition tritt an die Stelle der Definition materialer Wahrheit.

Diese Unterschiede sind im Projekt herauszuarbeiten, wobei im Detail die verschiedenen Varianten einer beweistheoretischen Semantik zu diskutieren sind. Die Untersuchungen zu den Punkten 1 und 3 erfordern vor allem Überlegungen von Inversionsprinzipien in der Logik, die Untersuchungen zu Punkt 2 vor allem die Erörterung des Verhältnisses von Logik und Struktur. Daher gliedert sich das Projekt in zwei Teilprojekte:

A) Inversionsprinzipien in der Logik

B) Logik und Struktur

Folgende Punkte sollen im ersten Teilprojekt bearbeitet werden:

Folgende Gesichtspunkte gehören zum zweiten Teilprojekt:

Zurück zur Homepage der Forschergruppe